Nuprl Lemma : rel-path_wf
11,40
postcript
pdf
T
:Type,
R
:(
T
T
),
L
:(
T
List). rel-path(
R
;
L
)
latex
Definitions
Type
,
t
T
,
s
=
t
,
,
x
:
A
B
(
x
)
,
type
List
,
||
as
||
,
n
+
m
,
-
n
,
n
-
m
,
a
<
b
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
,
{
x
:
A
|
B
(
x
)}
,
{
i
..
j
}
,
x
:
A
B
(
x
)
,
Void
,
x
:
A
.
B
(
x
)
,
l
[
i
]
,
f
(
a
)
,
x
f
y
,
#$n
,
rel-path(
R
;
L
)
Lemmas
int
seg
wf
,
length
wf1
,
select
wf
origin
T:Type, R:(T
T
), L:(T List). rel-path(R;L) 
T:Type, R:(TT), L:(T List). rel-path(R;L) TB(x)
Q
A
B j < k
}
B(x)x:A. B(x)